$\forall$${\it ds}$:fpf(Id; $x$.Type\{i\}), ${\it da}$:fpf(Knd; $k$.Type\{i\}). ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$) $\in$ Type\{i'\}